$\forall$$R$:Realizer. Rda($R$) $\in$ $k$:Knd fp$\rightarrow$ Type